1  /-
  2  Copyright (c) 2018 Mario Carneiro. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Mario Carneiro
  5  
  6  Archimedean groups and fields.
  7  -/
  8  import algebra.group_power algebra.field_power algebra.floor
src         └─────────────────┘ └─────────────────┘ └───────────┘
  9  import data.rat tactic.linarith
src         └──────┘ └─────────────┘
 10  
 11  variables {α : Type*}
id             
typ            
 12  
 13  open_locale add_monoid
 14  
 15  class archimedean (α) [ordered_comm_monoid α] : Prop :=
id                         └─────────────────┘ 
src                         └─────────────────┘
typ                        └─────────────────┘ 
doc                         └─────────────────┘
 16  (arch : ∀ (x : α) {y}, 0 < y → ∃ n : ℕ, x ≤ n • y)
id                                       
src                                           
typ                                      
 17  
 18  theorem exists_nat_gt [linear_ordered_semiring α] [archimedean α]
id                          └─────────────────────┘    └─────────┘ 
src                         └─────────────────────┘     └─────────┘
typ                         └─────────────────────┘    └─────────┘ 
 19    (x : α) : ∃ n : ℕ, x < n :=
id                      
src                      
typ                     
 20  let ⟨n, h⟩ := archimedean.arch x zero_lt_one in
id   └─┘          └──────────────┘  └─────────┘
src                └──────────────┘   └─────────┘
typ  └─┘          └──────────────┘  └─────────┘
 21  ⟨n+1, lt_of_le_of_lt (by rwa ← add_monoid.smul_one)
id        └────────────┘           └─────────────────┘
src       └────────────┘     └────┘└─────────────────┘
typ       └────────────┘     └────┘└─────────────────┘
doc                           └────┘
txt                           └────┘
par                           └────┘
pid                              └─┘
st                           └────────────────────────┘
 22    (nat.cast_lt.2 (nat.lt_succ_self _))⟩
id      └─────────┘   └──────────────┘
src     └─────────┘   └──────────────┘
typ     └─────────┘   └──────────────┘
 23  
 24  section linear_ordered_ring
 25  variables [linear_ordered_ring α] [archimedean α]
id              └─────────────────┘     └─────────┘
src             └─────────────────┘     └─────────┘
typ             └─────────────────┘     └─────────┘
 26  
 27  lemma pow_unbounded_of_one_lt (x : α) {y : α}
id                                             
typ                                            
 28      (hy1 : 1 < y) : ∃ n : ℕ, x < y ^ n :=
id                               
src                                
typ                              
 29  have hy0 : 0 < y - 1 := sub_pos_of_lt hy1,
id                        └───────────┘ └─┘
src                        └───────────┘
typ                       └───────────┘ └─┘
 30  -- TODO `by linarith` fails to prove hy1'
 31  have hy1' : (-1:α) ≤ y, from le_trans (neg_le_self zero_le_one) (le_of_lt hy1),
id                            └──────┘  └─────────┘ └─────────┘   └──────┘ └─┘
src                             └──────┘  └─────────┘ └─────────┘   └──────┘
typ                           └──────┘  └─────────┘ └─────────┘   └──────┘ └─┘
 32  let ⟨n, h⟩ := archimedean.arch x hy0 in
id   └─┘         └──────────────┘  └─┘
src                └──────────────┘
typ  └─┘         └──────────────┘  └─┘
 33  ⟨n, calc x ≤ n • (y - 1)     : h
id                    
src                     
typ                   
 34         ... < 1 + n • (y - 1) : lt_one_add _
id                              └────────┘
src                              └────────┘
typ                             └────────┘
 35         ... ≤ y ^ n           : one_add_sub_mul_le_pow hy1' n⟩
id                                └────────────────────┘ └──┘
src                                └────────────────────┘
typ                               └────────────────────┘ └──┘
doc                                 └────────────────────┘
 36  
 37  /-- Every x greater than 1 is between two successive natural-number
 38  powers of another y greater than one. -/
 39  lemma exists_nat_pow_near {x : α} {y : α} (hx : 1 < x) (hy : 1 < y) :
id                                                               
src                                                                
typ                                                              
 40    ∃ n : ℕ, y ^ n ≤ x ∧ x < y ^ (n + 1) :=
id                       
src                            
typ                      
 41  have h : ∃ n : ℕ, x < y ^ n, from pow_unbounded_of_one_lt _ hy,
id                             └─────────────────────┘   └┘
src                               └─────────────────────┘
typ                            └─────────────────────┘   └┘
 42  by classical; exact let n := nat.find h in
id                                └──────┘
src     └───────┘  └────┘   └────┘└──────┘ └───
typ     └───────┘  └────┘   └────┘└──────┘ └───
doc     └───────┘  └────┘   └────┘         └───
txt     └───────┘  └────┘   └────┘         └───
par     └───────┘  └────┘   └────┘         └───
pid                        └────┘         └───
st     └────────────────────────────────────────
 43    have hn  : x < y ^ n, from nat.find_spec h,
id                            └───────────┘ 
src  ─┘    └─────┘   └─────┘└───────────┘ └─
typ  ─┘    └─────┘ └─────┘└───────────┘└─
doc  ─┘    └─────┘     └─────┘              └─
txt  ─┘    └─────┘     └─────┘              └─
par  ─┘    └─────┘     └─────┘              └─
pid  ─┘    └─────┘     └─────┘              └─
st   ──────────────────────────────────────────────
 44    have hnp : 0 < n,     from nat.pos_iff_ne_zero.2 (λ hn0,
id                                └─────────────────┘
src  ─┘    └───────┘  └─────────┘└─────────────────┘└─┘  └─────
typ  ─┘    └───────┘  └─────────┘└─────────────────┘└─┘  └─────
doc  ─┘    └───────┘  └─────────┘                   └─┘  └─────
txt  ─┘    └───────┘  └─────────┘                   └─┘  └─────
par  ─┘    └───────┘  └─────────┘                   └─┘  └─────
pid  ─┘    └───────┘  └─────────┘                   └─┘  └─────
st   ───────────────────────────────────────────────────────────
 45      by rw [hn0, pow_zero] at hn; exact (not_lt_of_gt hn hx)),
id              └─┘  └──────┘                └──────────┘ └┘ └┘
src  ───┘  └──┘   └┘└──────┘└─────┘└──────┘ └──────────┘    └───
typ  ───┘  └──┘└─┘└┘└──────┘└─────┘└──────┘ └──────────┘└┘└┘└───
doc  ───┘  └──┘   └┘        └─────┘└──────┘                 └───
txt  ───┘  └──┘   └┘        └─────┘└──────┘                 └───
par  ───┘  └──┘   └┘        └─────┘└──────┘                 └───
pid  ───┘  └───┘   └┘        └─────────────┘                 └───
st   ─────┘└──────┘└────────┘└────────────────────────────────┘└──
 46    have hnsp : nat.pred n + 1 = n,     from nat.succ_pred_eq_of_pos hnp,
id                                            └─────────────────────┘
src  ─┘    └──────┘         └─┘ └─────────┘└─────────────────────┘   └─
typ  ─┘    └──────┘         └─┘ └─────────┘└─────────────────────┘   └─
doc  ─┘    └──────┘          └─┘  └─────────┘                          └─
txt  ─┘    └──────┘          └─┘  └─────────┘                          └─
par  ─┘    └──────┘          └─┘  └─────────┘                          └─
pid  ─┘    └──────┘          └─┘  └─────────┘                          └─
st   ────────────────────────────────────────────────────────────────────────
 47    have hltn : nat.pred n < n,         from nat.pred_lt (ne_of_gt hnp),
id                                              └─────────┘  └──────┘
src  ─┘    └──────┘           └─────────────┘└─────────┘ └──────┘   └──
typ  ─┘    └──────┘           └─────────────┘└─────────┘ └──────┘   └──
doc  ─┘    └──────┘           └─────────────┘                       └──
txt  ─┘    └──────┘           └─────────────┘                       └──
par  ─┘    └──────┘           └─────────────┘                       └──
pid  ─┘    └──────┘           └─────────────┘                       └──
st   ───────────────────────────────────────────────────────────────────────
 48    ⟨nat.pred n, le_of_not_lt (nat.find_min h hltn), by rwa hnsp⟩
id      └──────┘    └──────────┘  └──────────┘                 └──┘
src  ─┘ └──────┘ └┘└──────────┘ └──────────┘     └─┘  └──┘    └─
typ  ─┘ └──────┘ └┘└──────────┘ └──────────┘     └─┘  └──┘└──┘└─
doc  ─┘          └┘                              └─┘  └──┘    └─
txt  ─┘          └┘                              └─┘  └──┘    └─
par  ─┘          └┘                              └─┘  └──┘    └─
pid  ─┘          └┘                              └─┘  └───┘    
st   ────────────────────────────────────────────────────┘└───────┘└─
 49  
src  
typ  
doc  
txt  
par  
pid  
st   
 50  theorem exists_int_gt (x : α) : ∃ n : ℤ, x < n :=
id                                          
src                                          
typ                                         
 51  let ⟨n, h⟩ := exists_nat_gt x in ⟨n, by rwa ← coe_coe⟩
id   └─┘          └───────────┘                  └─────┘
src                └───────────┘             └────┘└─────┘
typ  └─┘          └───────────┘            └────┘└─────┘
doc                                          └────┘└─────┘
txt                                          └────┘
par                                          └────┘
pid                                             └─┘
st                                          └────────────┘
 52  
 53  theorem exists_int_lt (x : α) : ∃ n : ℤ, (n : α) < x :=
id                                               
src                                                
typ                                              
 54  let ⟨n, h⟩ := exists_int_gt (-x) in ⟨-n, by rw int.cast_neg; exact neg_lt.1 h⟩
id   └─┘          └───────────┘                 └──────────┘        └────┘   
src                └───────────┘               └─┘└──────────┘  └────┘└────┘└─┘
typ  └─┘          └───────────┘              └─┘└──────────┘  └────┘└────┘└─┘
doc                                              └─┘              └────┘      └─┘
txt                                              └─┘              └────┘      └─┘
par                                              └─┘              └────┘      └─┘
pid                                                                         └─┘
st                                              └────────────────────────────────┘
 55  
 56  theorem exists_floor (x : α) :
id                             
typ                            
 57    ∃ (fl : ℤ), ∀ (z : ℤ), z ≤ fl ↔ (z : α) ≤ x :=
id                          └┘         
src                                      
typ                         └┘         
 58  begin
st   └─────
 59    haveI := classical.prop_decidable,
id              └──────────────────────┘
src    └───────┘└──────────────────────┘
typ    └───────┘└──────────────────────┘
doc    └───────┘
txt    └───────┘
par    └───────┘
pid         └─┘
st   ──────────────────────────────────┘└─
 60    have : ∃ (ub : ℤ), (ub:α) ≤ x ∧ ∀ (z : ℤ), (z:α) ≤ x → z ≤ ub :=
id                                                   
src    └─────┘└─────┘     └┘  └────┘     └┘       └───
typ    └─────┘└─────┘     └┘  └────┘    └┘      └───
doc    └─────┘ └─────┘      └┘    └────┘     └┘       └───
txt    └─────┘ └─────┘      └┘    └────┘     └┘       └───
par    └─────┘ └─────┘      └┘    └────┘     └┘       └───
pid    └───┘└┘ └─────┘      └┘    └────┘     └┘       └───
st   ───────────────────────────────────────────────────────────────────
 61    int.exists_greatest_of_bdd
id     └────────────────────────┘
src  ─┘└────────────────────────┘
typ  ─┘└────────────────────────┘
doc  ─┘                          
txt  ─┘                          
par  ─┘                          
pid  ─┘                          
st   ─────────────────────────────
 62      (let ⟨n, hn⟩ := exists_int_gt x in ⟨n, λ z h',
id               └┘     └───────────┘
src  ───┘      └┘  └───┘└───────────┘ └──┘  └┘ └──────
typ  ───┘     └┘└┘└───┘└───────────┘ └──┘  └┘ └──────
doc  ───┘      └┘  └───┘              └──┘  └┘ └──────
txt  ───┘      └┘  └───┘              └──┘  └┘ └──────
par  ───┘      └┘  └───┘              └──┘  └┘ └──────
pid  ───┘      └┘  └───┘              └──┘  └┘ └──────
st   ───────────────────────────────────────────────────
 63        int.cast_le.1 $ le_trans h' $ le_of_lt hn⟩)
id         └─────────┘     └──────┘
src  ─────┘└─────────┘└─┘ └──────┘             └──
typ  ─────┘└─────────┘└─┘ └──────┘             └──
doc  ─────┘           └─┘                      └──
txt  ─────┘           └─┘                      └──
par  ─────┘           └─┘                      └──
pid  ─────┘           └─┘                      └──
st   ──────────────────────────────────────────────────
 64      (let ⟨n, hn⟩ := exists_int_lt x in ⟨n, le_of_lt hn⟩),
id               └┘     └───────────┘         └──────┘
src  ───┘      └┘  └───┘└───────────┘ └──┘  └┘└──────┘  └┘
typ  ───┘     └┘└┘└───┘└───────────┘└──┘  └┘└──────┘  └┘
doc  ───┘      └┘  └───┘              └──┘  └┘          └┘
txt  ───┘      └┘  └───┘              └──┘  └┘          └┘
par  ───┘      └┘  └───┘              └──┘  └┘          └┘
pid  ───┘      └┘  └───┘              └──┘  └┘          └┘
st   ───────────────────────────────────────────────────────┘└─
 65    refine this.imp (λ fl h z, _),
id            └──────┘
src    └─────┘└──────┘  └─────────┘
typ    └─────┘└──────┘  └─────────┘
doc    └─────┘          └─────────┘
txt    └─────┘          └─────────┘
par    └─────┘          └─────────┘
pid                    └─────────┘
st   ──────────────────────────────┘└─
 66    cases h with h₁ h₂,
id           
src    └────┘ └─────────┘
typ    └────┘└─────────┘
doc    └────┘ └─────────┘
txt    └────┘ └─────────┘
par    └────┘ └─────────┘
pid          └─────────┘
st   ───────────────────┘└─
 67    exact ⟨λ h, le_trans (int.cast_le.2 h) h₁, h₂ z⟩,
id                 └──────┘  └─────────┘      └┘  └┘ 
src    └────┘  └──┘└──────┘ └─────────┘└─┘ └┘  └┘   
typ    └────┘  └──┘└──────┘ └─────────┘└─┘ └┘└┘└┘└┘
doc    └────┘  └──┘                    └─┘ └┘  └┘   
txt    └────┘  └──┘                    └─┘ └┘  └┘   
par    └────┘  └──┘                    └─┘ └┘  └┘   
pid           └──┘                    └─┘ └┘  └┘   
st   ─────────────────────────────────────────────────┘└─
 68  end
st   ──┘
 69  
 70  end linear_ordered_ring
 71  
 72  section linear_ordered_field
 73  
 74  /-- Every positive x is between two successive integer powers of
 75  another y greater than one. This is the same as `exists_int_pow_near'`,
 76  but with ≤ and < the other way around. -/
 77  lemma exists_int_pow_near [discrete_linear_ordered_field α] [archimedean α]
id                              └───────────────────────────┘    └─────────┘ 
src                             └───────────────────────────┘     └─────────┘
typ                             └───────────────────────────┘    └─────────┘ 
 78    {x : α} {y : α} (hx : 0 < x) (hy : 1 < y) :
id                                       
src                                        
typ                                      
 79    ∃ n : ℤ, y ^ n ≤ x ∧ x < y ^ (n + 1) :=
id                       
src                            
typ                      
 80  by classical; exact
src     └───────┘  └────┘
typ     └───────┘  └────┘
doc     └───────┘  └────┘
txt     └───────┘  └────┘
par     └───────┘  └────┘
pid                     
st     └─────────────────
 81  let ⟨N, hN⟩ := pow_unbounded_of_one_lt x⁻¹ hy in
id                 └─────────────────────┘ └┘ └┘
src       └┘  └───┘└─────────────────────┘ └┘  └───
typ      └┘  └───┘└─────────────────────┘└┘└┘└───
doc       └┘  └───┘                            └───
txt       └┘  └───┘                            └───
par       └┘  └───┘                            └───
pid       └┘  └───┘                            └───
st   ─────────────────────────────────────────────────
 82    have he: ∃ m : ℤ, y ^ m ≤ x, from
id                          
src  ─┘    └───┘└───┘    └──────
typ  ─┘    └───┘└───┘    └──────
doc  ─┘    └───┘ └───┘       └──────
txt  ─┘    └───┘ └───┘       └──────
par  ─┘    └───┘ └───┘       └──────
pid  ─┘    └───┘ └───┘       └──────
st   ────────────────────────────────────
 83      ⟨-N, le_of_lt (by rw [(fpow_neg y (↑N)), one_div_eq_inv];
id           └──────┘          └──────┘       └────────────┘
src  ───┘  └┘└──────┘   └──┘ └──────┘   └──┘└────────────┘└─
typ  ───┘  └┘└──────┘   └──┘ └──────┘ └──┘└────────────┘└─
doc  ───┘   └┘           └──┘             └──┘              └─
txt  ───┘   └┘           └──┘             └──┘              └─
par  ───┘   └┘           └──┘             └──┘              └─
pid  ───┘   └┘           └───┘             └──┘              └──
st   ────────────────────┘└────────────────────┘└──────────────┘└─
 84      exact (inv_lt hx (lt_trans (inv_pos hx) hN)).1 hN)⟩,
id              └────┘     └──────┘  └─────┘ └┘         └┘
src  ─────────┘ └────┘   └──────┘ └─────┘  └┘  └───┘  └──┘
typ  ─────────┘ └────┘   └──────┘ └─────┘└┘└┘  └───┘└┘└──┘
doc  ─────────┘                            └┘  └───┘  └──┘
txt  ─────────┘                            └┘  └───┘  └──┘
par  ─────────┘                            └┘  └───┘  └──┘
pid  ─────────┘                            └┘  └───┘  └──┘
st   ────────────────────────────────────────────────────┘└───
 85  let ⟨M, hM⟩ := pow_unbounded_of_one_lt x hy in
id          └┘
src       └┘  └───┘                          └───
typ      └┘└┘└───┘                          └───
doc       └┘  └───┘                          └───
txt       └┘  └───┘                          └───
par       └┘  └───┘                          └───
pid       └┘  └───┘                          └───
st   ───────────────────────────────────────────────
 86    have hb: ∃ b : ℤ, ∀ m, y ^ m ≤ x → m ≤ b, from
id                            
src  ─┘    └───┘ └───┘   └┘          └──────
typ  ─┘    └───┘ └───┘   └┘         └──────
doc  ─┘    └───┘ └───┘   └┘          └──────
txt  ─┘    └───┘ └───┘   └┘          └──────
par  ─┘    └───┘ └───┘   └┘          └──────
pid  ─┘    └───┘ └───┘   └┘          └──────
st   ─────────────────────────────────────────────────
 87      ⟨M, λ m hm, le_of_not_lt (λ hlt, not_lt_of_ge
id                   └──────────┘         └──────────┘
src  ───┘  └┘ └─────┘└──────────┘  └────┘└──────────┘
typ  ───┘  └┘ └─────┘└──────────┘  └────┘└──────────┘
doc  ───┘  └┘ └─────┘              └────┘            
txt  ───┘  └┘ └─────┘              └────┘            
par  ───┘  └┘ └─────┘              └────┘            
pid  ───┘  └┘ └─────┘              └────┘            
st   ──────────────────────────────────────────────────
 88    (fpow_le_of_le (le_of_lt hy) (le_of_lt hlt)) (lt_of_le_of_lt hm hM))⟩,
id      └───────────┘                                └────────────┘
src  ─┘ └───────────┘           └┘            └─┘ └────────────┘    └───┘
typ  ─┘ └───────────┘           └┘            └─┘ └────────────┘    └───┘
doc  ─┘                         └┘            └─┘                   └───┘
txt  ─┘                         └┘            └─┘                   └───┘
par  ─┘                         └┘            └─┘                   └───┘
pid  ─┘                         └┘            └─┘                   └───┘
st   ─────────────────────────────────────────────────────────────────────────
 89  let ⟨n, hn₁, hn₂⟩ := int.exists_greatest_of_bdd hb he in
id          └─┘  └─┘     └────────────────────────┘
src       └┘   └┘   └───┘└────────────────────────┘    └───
typ      └┘└─┘└┘└─┘└───┘└────────────────────────┘    └───
doc       └┘   └┘   └───┘                              └───
txt       └┘   └┘   └───┘                              └───
par       └┘   └┘   └───┘                              └───
pid       └┘   └┘   └───┘                              └───
st   ─────────────────────────────────────────────────────────
 90    ⟨n, hn₁, lt_of_not_ge (λ hge, not_le_of_gt (int.lt_succ _) (hn₂ _ hge))⟩
id              └──────────┘         └──────────┘  └─────────┘
src  ─┘  └┘   └┘└──────────┘  └────┘└──────────┘ └─────────┘└──┘    └─┘   └───
typ  ─┘  └┘   └┘└──────────┘  └────┘└──────────┘ └─────────┘└──┘    └─┘   └───
doc  ─┘  └┘   └┘              └────┘                        └──┘    └─┘   └───
txt  ─┘  └┘   └┘              └────┘                        └──┘    └─┘   └───
par  ─┘  └┘   └┘              └────┘                        └──┘    └─┘   └───
pid  ─┘  └┘   └┘              └────┘                        └──┘    └─┘   └─┘
st   ───────────────────────────────────────────────────────────────────────────
 91  
src  
typ  
doc  
txt  
par  
pid  
st   
 92  /-- Every positive x is between two successive integer powers of
 93  another y greater than one. This is the same as `exists_int_pow_near`,
 94  but with ≤ and < the other way around. -/
 95  lemma exists_int_pow_near' [discrete_linear_ordered_field α] [archimedean α]
id                               └───────────────────────────┘    └─────────┘ 
src                              └───────────────────────────┘     └─────────┘
typ                              └───────────────────────────┘    └─────────┘ 
 96    {x : α} {y : α} (hx : 0 < x) (hy : 1 < y) :
id                                       
src                                        
typ                                      
 97    ∃ n : ℤ, y ^ n < x ∧ x ≤ y ^ (n + 1) :=
id                       
src                            
typ                      
 98  let ⟨m, hle, hlt⟩ := exists_int_pow_near (inv_pos hx) hy in
id   └─┘                 └─────────────────┘  └─────┘ └┘  └┘
src                       └─────────────────┘  └─────┘
typ  └─┘                 └─────────────────┘  └─────┘ └┘  └┘
doc                       └─────────────────┘
 99  have hyp : 0 < y, from lt_trans (discrete_linear_ordered_field.zero_lt_one α) hy,
id                        └──────┘  └───────────────────────────────────────┘   └┘
src                        └──────┘  └───────────────────────────────────────┘
typ                       └──────┘  └───────────────────────────────────────┘   └┘
100  ⟨-(m+1),
id      
src     
typ     
101  by rwa [fpow_neg, one_div_eq_inv, inv_lt (fpow_pos_of_pos hyp _) hx],
id           └──────┘  └────────────┘  └────┘  └─────────────┘ └─┘    └┘
src     └───┘└──────┘└┘└────────────┘└┘└────┘ └─────────────┘   └──┘  
typ     └───┘└──────┘└┘└────────────┘└┘└────┘ └─────────────┘└─┘└──┘└┘
doc     └───┘        └┘              └┘                         └──┘  
txt     └───┘        └┘              └┘                         └──┘  
par     └───┘        └┘              └┘                         └──┘  
pid        └┘        └┘              └┘                         └──┘  
st     └────────────┘└──────────────┘└─────────────────────────────────┘
102  by rwa [neg_add, neg_add_cancel_right, fpow_neg, one_div_eq_inv,
id           └─────┘  └──────────────────┘  └──────┘  └────────────┘
src     └───┘└─────┘└┘└──────────────────┘└┘└──────┘└┘└────────────┘└─
typ     └───┘└─────┘└┘└──────────────────┘└┘└──────┘└┘└────────────┘└─
doc     └───┘       └┘                    └┘        └┘              └─
txt     └───┘       └┘                    └┘        └┘              └─
par     └───┘       └┘                    └┘        └┘              └─
pid        └┘       └┘                    └┘        └┘              └─
st     └───────────┘└────────────────────┘└────────┘└──────────────┘└─
103          le_inv hx (fpow_pos_of_pos hyp _)]⟩
id           └────┘ └┘  └─────────────┘ └─┘
src  ───────┘└────┘   └─────────────┘   └──┘
typ  ───────┘└────┘└┘ └─────────────┘└─┘└──┘
doc  ───────┘                           └──┘
txt  ───────┘                           └──┘
par  ───────┘                           └──┘
pid  ───────┘                           └──┘
st   ────────────────────────────────────────┘
104  
105  variables [linear_ordered_field α] [floor_ring α]
id              └──────────────────┘     └────────┘
src             └──────────────────┘     └────────┘
typ             └──────────────────┘     └────────┘
doc                                      └────────┘
106  
107  lemma sub_floor_div_mul_nonneg (x : α) {y : α} (hy : 0 < y) :
id                                                         
src                                                         
typ                                                        
108    0 ≤ x - ⌊x / y⌋ * y :=
id              
src               
typ             
doc                 
109  begin
st   └─────
110    conv in x {rw ← div_mul_cancel x (ne_of_lt hy).symm},
id                    └────────────┘   └──────┘ └┘
src    └──────┘ └┘└───┘└────────────┘  └──────┘  └────┘
typ    └──────┘└┘└───┘└────────────┘ └──────┘└┘└────┘
txt    └──────┘ └┘└───┘                          └────┘
par    └──────┘ └┘└───┘                          └────┘
pid        └─┘ └─────┘                          └─────┘
st   ────────────┘└──────────────────────────────────────┘└┘
111    rw ← sub_mul,
id          └─────┘
src    └───┘└─────┘
typ    └───┘└─────┘
doc    └───┘
txt    └───┘
par    └───┘
pid      └─┘
st   ─────────────┘└─
112    exact mul_nonneg (sub_nonneg.2 (floor_le _)) (le_of_lt hy)
id           └────────┘  └────────┘    └──────┘      └──────┘ └┘
src    └────┘└────────┘ └────────┘└─┘ └──────┘└───┘ └──────┘  └┘
typ    └────┘└────────┘ └────────┘└─┘ └──────┘└───┘ └──────┘└┘└┘
doc    └────┘                     └─┘         └───┘           └┘
txt    └────┘                     └─┘         └───┘           └┘
par    └────┘                     └─┘         └───┘           └┘
pid                              └─┘         └───┘           
st   ────────────────────────────────────────────────────────────┘
113  end
st   └─┘
114  
115  lemma sub_floor_div_mul_lt (x : α) {y : α} (hy : 0 < y) :
id                                                     
src                                                     
typ                                                    
116    x - ⌊x / y⌋ * y < y :=
id             
src               
typ            
doc             
117  sub_lt_iff_lt_add.2 begin
id   └───────────────┘
src  └───────────────┘
typ  └───────────────┘
st                       └─────
118    conv in y {rw ← one_mul y},
id                    └─────┘ 
src    └──────┘ └┘└───┘└─────┘ 
typ    └──────┘└┘└───┘└─────┘
txt    └──────┘ └┘└───┘        
par    └──────┘ └┘└───┘        
pid        └─┘ └─────┘        
st   ────────────┘└────────────┘└┘
119    conv in x {rw ← div_mul_cancel x (ne_of_lt hy).symm},
id                    └────────────┘   └──────┘ └┘
src    └──────┘ └┘└───┘└────────────┘  └──────┘  └────┘
typ    └──────┘└┘└───┘└────────────┘ └──────┘└┘└────┘
txt    └──────┘ └┘└───┘                          └────┘
par    └──────┘ └┘└───┘                          └────┘
pid        └─┘ └─────┘                          └─────┘
st   ────────────┘└──────────────────────────────────────┘└┘
120    rw ← add_mul,
id          └─────┘
src    └───┘└─────┘
typ    └───┘└─────┘
doc    └───┘
txt    └───┘
par    └───┘
pid      └─┘
st   ─────────────┘└─
121    exact (mul_lt_mul_right hy).2 (by rw add_comm; exact lt_floor_add_one _),
id            └──────────────┘ └┘           └──────┘        └──────────────┘
src    └────┘ └──────────────┘  └──┘   └─┘└──────┘└──────┘└──────────────┘└─┘
typ    └────┘ └──────────────┘└┘└──┘   └─┘└──────┘└──────┘└──────────────┘└─┘
doc    └────┘                   └──┘   └─┘        └──────┘                └─┘
txt    └────┘                   └──┘   └─┘        └──────┘                └─┘
par    └────┘                   └──┘   └─┘        └──────┘                └─┘
pid                            └──┘   └──┘        └──────┘                └─┘
st   ──────────────────────────────────┘└────────────────────────────────────┘└─
122  end
st   ──┘
123  
124  end linear_ordered_field
125  
126  instance : archimedean ℕ :=
id              └─────────┘ 
src             └─────────┘ 
typ             └─────────┘ 
127  ⟨λ n m m0, ⟨n, by simpa only [mul_one, nat.smul_eq_mul] using nat.mul_le_mul_left n m0⟩⟩
id        └┘                    └─────┘  └─────────────┘        └─────────────────┘  └┘
src                    └──────────┘└─────┘└┘└─────────────┘└──────┘└─────────────────┘ 
typ       └┘        └──────────┘└─────┘└┘└─────────────┘└──────┘└─────────────────┘└┘
doc                    └──────────┘       └┘               └──────┘                    
txt                    └──────────┘       └┘               └──────┘                    
par                    └──────────┘       └┘               └──────┘                    
pid                         └──┘└┘       └┘               └────┘                    
st                    └───────────────────────────────────────────────────────────────────┘
128  
129  instance : archimedean ℤ :=
id              └─────────┘ 
src             └─────────┘ 
typ             └─────────┘ 
130  ⟨λ n m m0, ⟨n.to_nat, le_trans (int.le_to_nat _) $
id        └┘   └─────┘  └──────┘  └───────────┘
src               └─────┘  └──────┘  └───────────┘
typ       └┘   └─────┘  └──────┘  └───────────┘
131  by simpa only [add_monoid.smul_eq_mul, int.nat_cast_eq_coe_nat, zero_add, mul_one] using mul_le_mul_of_nonneg_left
id                  └────────────────────┘  └─────────────────────┘  └──────┘  └─────┘        └───────────────────────┘
src     └──────────┘└────────────────────┘└┘└─────────────────────┘└┘└──────┘└┘└─────┘└──────┘└───────────────────────┘
typ     └──────────┘└────────────────────┘└┘└─────────────────────┘└┘└──────┘└┘└─────┘└──────┘└───────────────────────┘
doc     └──────────┘                      └┘                       └┘        └┘       └──────┘                         
txt     └──────────┘                      └┘                       └┘        └┘       └──────┘                         
par     └──────────┘                      └┘                       └┘        └┘       └──────┘                         
pid          └──┘└┘                      └┘                       └┘        └┘       └────┘                         
st     └────────────────────────────────────────────────────────────────────────────────────────────────────────────────
132      (int.add_one_le_iff.2 m0) (int.coe_zero_le n.to_nat)⟩⟩
id        └────────────────┘   └┘   └─────────────┘ └──────┘
src  ───┘ └────────────────┘└─┘  └┘ └─────────────┘└──────┘
typ  ───┘ └────────────────┘└─┘└┘└┘ └─────────────┘└──────┘
doc  ───┘                   └─┘  └┘                        
txt  ───┘                   └─┘  └┘                        
par  ───┘                   └─┘  └┘                        
pid  ───┘                   └─┘  └┘                        
st   ───────────────────────────────────────────────────────┘
133  
134  noncomputable def archimedean.floor_ring (α)
135    [linear_ordered_ring α] [archimedean α] : floor_ring α :=
id      └─────────────────┘    └─────────┘     └────────┘ 
src     └─────────────────┘     └─────────┘      └────────┘
typ     └─────────────────┘    └─────────┘     └────────┘ 
doc                                              └────────┘
136  { floor := λ x, classical.some (exists_floor x),
id                  └────────────┘  └──────────┘ 
src                  └────────────┘  └──────────┘
typ                 └────────────┘  └──────────┘ 
137    le_floor := λ z x, classical.some_spec (exists_floor x) z }
id                      └─────────────────┘  └──────────┘   
src                       └─────────────────┘  └──────────┘
typ                     └─────────────────┘  └──────────┘   
138  
139  section linear_ordered_field
140  variables [linear_ordered_field α]
id              └──────────────────┘
src             └──────────────────┘
typ             └──────────────────┘
141  
142  theorem archimedean_iff_nat_lt :
143    archimedean α ↔ ∀ x : α, ∃ n : ℕ, x < n :=
id     └─────────┘                   
src    └─────────┘                     
typ    └─────────┘                   
144  ⟨@exists_nat_gt α _, λ H, ⟨λ x y y0,
id     └───────────┘              └┘
src    └───────────┘
typ    └───────────┘              └┘
145    (H (x / y)).imp $ λ n h, le_of_lt $
id            └─┘         └──────┘
src              └─┘           └──────┘
typ           └─┘         └──────┘
146    by rwa [div_lt_iff y0, ← add_monoid.smul_eq_mul] at h⟩⟩
id             └────────┘ └┘    └────────────────────┘
src       └───┘└────────┘  └──┘└────────────────────┘└────┘
typ       └───┘└────────┘└┘└──┘└────────────────────┘└────┘
doc       └───┘            └──┘                      └────┘
txt       └───┘            └──┘                      └────┘
par       └───┘            └──┘                      └────┘
pid          └┘            └──┘                      └───┘
st       └─────────────────┘└────────────────────────┘└───┘
147  
148  theorem archimedean_iff_nat_le :
149    archimedean α ↔ ∀ x : α, ∃ n : ℕ, x ≤ n :=
id     └─────────┘                   
src    └─────────┘                     
typ    └─────────┘                   
150  archimedean_iff_nat_lt.trans
id   └────────────────────┘└────┘
src  └────────────────────┘└────┘
typ  └────────────────────┘└────┘
151  ⟨λ H x, (H x).imp $ λ _, le_of_lt,
id            └─┘        └──────┘
src               └─┘         └──────┘
typ           └─┘        └──────┘
152   λ H x, let ⟨n, h⟩ := H x in ⟨n+1,
id         └─┘                
src                                 
typ        └─┘                
153     lt_of_le_of_lt h (nat.cast_lt.2 (lt_add_one _))⟩⟩
id      └────────────┘    └─────────┘   └────────┘
src     └────────────┘    └─────────┘   └────────┘
typ     └────────────┘    └─────────┘   └────────┘
154  
155  theorem exists_rat_gt [archimedean α] (x : α) : ∃ q : ℚ, x < q :=
id                          └─────────┘                    
src                         └─────────┘                      
typ                         └─────────┘                    
doc                                                        
156  let ⟨n, h⟩ := exists_nat_gt x in ⟨n, by rwa rat.cast_coe_nat⟩
id   └─┘          └───────────┘                └──────────────┘
src                └───────────┘             └──┘└──────────────┘
typ  └─┘          └───────────┘            └──┘└──────────────┘
doc                                          └──┘
txt                                          └──┘
par                                          └──┘
pid                                             
st                                          └───────────────────┘
157  
158  theorem archimedean_iff_rat_lt :
159    archimedean α ↔ ∀ x : α, ∃ q : ℚ, x < q :=
id     └─────────┘                   
src    └─────────┘                     
typ    └─────────┘                   
doc                                   
160  ⟨@exists_rat_gt α _,
id     └───────────┘ 
src    └───────────┘
typ    └───────────┘ 
161    λ H, archimedean_iff_nat_lt.2 $ λ x,
id         └────────────────────┘      
src         └────────────────────┘
typ        └────────────────────┘      
162    let ⟨q, h⟩ := H x in
id     └─┘          
typ    └─┘          
163    ⟨nat_ceil q, lt_of_lt_of_le h $
id      └──────┘    └────────────┘
src     └──────┘    └────────────┘
typ     └──────┘    └────────────┘
doc     └──────┘
164      by simpa only [rat.cast_coe_nat] using (@rat.cast_le α _ _ _).2 (le_nat_ceil _)⟩⟩
id                      └──────────────┘          └─────────┘            └─────────┘
src         └──────────┘└──────────────┘└──────┘  └─────────┘ └────────┘ └─────────┘└─┘
typ         └──────────┘└──────────────┘└──────┘  └─────────┘└────────┘ └─────────┘└─┘
doc         └──────────┘                └──────┘              └────────┘            └─┘
txt         └──────────┘                └──────┘              └────────┘            └─┘
par         └──────────┘                └──────┘              └────────┘            └─┘
pid              └──┘└┘                └────┘              └────────┘            └─┘
st         └───────────────────────────────────────────────────────────────────────────┘
165  
166  theorem archimedean_iff_rat_le :
167    archimedean α ↔ ∀ x : α, ∃ q : ℚ, x ≤ q :=
id     └─────────┘                   
src    └─────────┘                     
typ    └─────────┘                   
doc                                   
168  archimedean_iff_rat_lt.trans
id   └────────────────────┘└────┘
src  └────────────────────┘└────┘
typ  └────────────────────┘└────┘
169  ⟨λ H x, (H x).imp $ λ _, le_of_lt,
id            └─┘        └──────┘
src               └─┘         └──────┘
typ           └─┘        └──────┘
170   λ H x, let ⟨n, h⟩ := H x in ⟨n+1,
id         └─┘                
src                                 
typ        └─┘                
171     lt_of_le_of_lt h (rat.cast_lt.2 (lt_add_one _))⟩⟩
id      └────────────┘    └─────────┘   └────────┘
src     └────────────┘    └─────────┘   └────────┘
typ     └────────────┘    └─────────┘   └────────┘
172  
173  variable [archimedean α]
id             └─────────┘
src            └─────────┘
typ            └─────────┘
174  
175  theorem exists_rat_lt (x : α) : ∃ q : ℚ, (q : α) < x :=
id                                               
src                                                
typ                                              
doc                                        
176  let ⟨n, h⟩ := exists_int_lt x in ⟨n, by rwa rat.cast_coe_int⟩
id   └─┘          └───────────┘                └──────────────┘
src                └───────────┘             └──┘└──────────────┘
typ  └─┘          └───────────┘            └──┘└──────────────┘
doc                                          └──┘
txt                                          └──┘
par                                          └──┘
pid                                             
st                                          └───────────────────┘
177  
178  theorem exists_rat_btwn {x y : α} (h : x < y) : ∃ q : ℚ, x < q ∧ (q:α) < y :=
id                                                              
src                                                                   
typ                                                             
doc                                                        
179  begin
st   └─────
180    cases exists_nat_gt (y - x)⁻¹ with n nh,
id           └───────────┘     └┘
src    └────┘└───────────┘   └┘└────────┘
typ    └────┘└───────────┘ └┘└────────┘
doc    └────┘                   └────────┘
txt    └────┘                   └────────┘
par    └────┘                   └────────┘
pid                            └────────┘
st   ────────────────────────────────────────┘└─
181    cases exists_floor (x * n) with z zh,
id           └──────────┘    
src    └────┘└──────────┘   └─────────┘
typ    └────┘└──────────┘ └─────────┘
doc    └────┘                └─────────┘
txt    └────┘                └─────────┘
par    └────┘                └─────────┘
pid                         └────────┘
st   ─────────────────────────────────────┘└─
182    refine ⟨(z + 1 : ℤ) / n, _⟩,
id                        
src    └─────┘   └───┘ └┘ └──┘
typ    └─────┘  └───┘ └┘└──┘
doc    └─────┘    └───┘ └┘  └──┘
txt    └─────┘    └───┘ └┘  └──┘
par    └─────┘    └───┘ └┘  └──┘
pid              └───┘ └┘  └──┘
st   ────────────────────────────┘└─
183    have n0 := nat.cast_pos.1 (lt_trans (inv_pos (sub_pos.2 h)) nh),
id                └──────────┘    └──────┘  └─────┘  └─────┘      └┘
src    └─────────┘└──────────┘└─┘ └──────┘ └─────┘ └─────┘└─┘ └─┘  
typ    └─────────┘└──────────┘└─┘ └──────┘ └─────┘ └─────┘└─┘└─┘└┘
doc    └─────────┘            └─┘                         └─┘ └─┘  
txt    └─────────┘            └─┘                         └─┘ └─┘  
par    └─────────┘            └─┘                         └─┘ └─┘  
pid    └─────┘└─┘            └─┘                         └─┘ └─┘  
st   ────────────────────────────────────────────────────────────────┘└─
184    have n0' := (@nat.cast_pos α _ _).2 n0,
id                   └──────────┘         └┘
src    └──────────┘  └──────────┘ └──────┘
typ    └──────────┘  └──────────┘└──────┘└┘
doc    └──────────┘               └──────┘
txt    └──────────┘               └──────┘
par    └──────────┘               └──────┘
pid    └──────┘└─┘               └──────┘
st   ───────────────────────────────────────┘└─
185    rw [rat.cast_div_of_ne_zero, rat.cast_coe_nat, rat.cast_coe_int, div_lt_iff n0'],
id         └─────────────────────┘  └──────────────┘  └──────────────┘  └────────┘ └─┘
src    └──┘└─────────────────────┘└┘└──────────────┘└┘└──────────────┘└┘└────────┘   
typ    └──┘└─────────────────────┘└┘└──────────────┘└┘└──────────────┘└┘└────────┘└─┘
doc    └──┘                       └┘                └┘                └┘             
txt    └──┘                       └┘                └┘                └┘             
par    └──┘                       └┘                └┘                └┘             
pid      └┘                       └┘                └┘                └┘             
st   ────────────────────────────┘└────────────────┘└────────────────┘└──────────────┘└──
186    refine ⟨(lt_div_iff n0').2 $
id              └────────┘ └─┘
src    └─────┘  └────────┘   └──┘ 
typ    └─────┘  └────────┘└─┘└──┘ 
doc    └─────┘               └──┘ 
txt    └─────┘               └──┘ 
par    └─────┘               └──┘ 
pid                         └──┘ 
st   ───────────────────────────────
187      (lt_iff_lt_of_le_iff_le (zh _)).1 (lt_add_one _), _⟩,
id        └────────────────────┘  └┘        └────────┘
src  ───┘ └────────────────────┘   └─────┘ └────────┘└─────┘
typ  ───┘ └────────────────────┘ └┘└─────┘ └────────┘└─────┘
doc  ───┘                          └─────┘           └─────┘
txt  ───┘                          └─────┘           └─────┘
par  ───┘                          └─────┘           └─────┘
pid  ───┘                          └─────┘           └─────┘
st   ───────────────────────────────────────────────────────┘└─
188    rw [int.cast_add, int.cast_one],
id         └──────────┘  └──────────┘
src    └──┘└──────────┘└┘└──────────┘
typ    └──┘└──────────┘└┘└──────────┘
doc    └──┘            └┘            
txt    └──┘            └┘            
par    └──┘            └┘            
pid      └┘            └┘            
st   ─────────────────┘└────────────┘└──
189    refine lt_of_le_of_lt (add_le_add_right ((zh _).1 (le_refl _)) _) _,
id            └────────────┘  └──────────────┘   └┘       └─────┘
src    └─────┘└────────────┘ └──────────────┘    └────┘ └─────┘└───────┘
typ    └─────┘└────────────┘ └──────────────┘  └┘└────┘ └─────┘└───────┘
doc    └─────┘                                   └────┘        └───────┘
txt    └─────┘                                   └────┘        └───────┘
par    └─────┘                                   └────┘        └───────┘
pid                                             └────┘        └───────┘
st   ────────────────────────────────────────────────────────────────────┘└─
190    rwa [← lt_sub_iff_add_lt', ← sub_mul,
id            └────────────────┘    └─────┘
src    └─────┘└────────────────┘└──┘└─────┘└─
typ    └─────┘└────────────────┘└──┘└─────┘└─
doc    └─────┘                  └──┘       └─
txt    └─────┘                  └──┘       └─
par    └─────┘                  └──┘       └─
pid       └──┘                  └──┘       └─
st   ──────────────────────────┘└─────────┘└─
191         ← div_lt_iff' (sub_pos.2 h), one_div_eq_inv],
id            └─────────┘  └─────┘      └────────────┘
src  ────────┘└─────────┘ └─────┘└─┘ └─┘└────────────┘
typ  ────────┘└─────────┘ └─────┘└─┘└─┘└────────────┘
doc  ────────┘                   └─┘ └─┘              
txt  ────────┘                   └─┘ └─┘              
par  ────────┘                   └─┘ └─┘              
pid  ────────┘                   └─┘ └─┘              
st   ─────────────────────────────────┘└──────────────┘└─
192    { rw [rat.coe_int_denom, nat.cast_one], exact one_ne_zero },
id           └───────────────┘  └──────────┘         └─────────┘
src      └──┘└───────────────┘└┘└──────────┘  └────┘└─────────┘
typ      └──┘└───────────────┘└┘└──────────┘  └────┘└─────────┘
doc      └──┘                 └┘              └────┘           
txt      └──┘                 └┘              └────┘           
par      └──┘                 └┘              └────┘           
pid        └┘                 └┘                              
st   ───┘└───────────────────┘└────────────┘└───────────────────┘└┘
193    { intro H, rw [rat.coe_nat_num, ← coe_coe, nat.cast_eq_zero] at H, subst H, cases n0 },
id                    └─────────────┘    └─────┘  └──────────────┘                      └┘
src      └─────┘  └──┘└─────────────┘└──┘└─────┘└┘└──────────────┘└────┘  └────┘   └────┘  
typ      └─────┘  └──┘└─────────────┘└──┘└─────┘└┘└──────────────┘└────┘  └────┘  └────┘└┘
doc      └─────┘  └──┘               └──┘└─────┘└┘                └────┘  └────┘   └────┘  
txt      └─────┘  └──┘               └──┘       └┘                └────┘  └────┘   └────┘  
par      └─────┘  └──┘               └──┘       └┘                └────┘  └────┘   └────┘  
pid           └┘    └┘               └──┘       └┘                └───┘                 
st   ───┘└─────┘└───────────────────┘└─────────┘└────────────────┘└───┘└───────┘└─────────┘└┘
194    { rw [rat.coe_nat_denom, nat.cast_one], exact one_ne_zero }
id           └───────────────┘  └──────────┘         └─────────┘
src      └──┘└───────────────┘└┘└──────────┘  └────┘└─────────┘
typ      └──┘└───────────────┘└┘└──────────┘  └────┘└─────────┘
doc      └──┘                 └┘              └────┘           
txt      └──┘                 └┘              └────┘           
par      └──┘                 └┘              └────┘           
pid        └┘                 └┘                              
st   ────────────────────────┘└────────────┘└───────────────────┘└─
195  end
st   ──┘
196  
197  theorem exists_nat_one_div_lt {ε : α} (hε : 0 < ε) : ∃ n : ℕ, 1 / (n + 1: α) < ε :=
id                                                                       
src                                                                         
typ                                                                      
198  begin
st   └─────
199    cases archimedean_iff_nat_lt.1 (by apply_instance) (1/ε) with n hn,
id           └────────────────────┘                         
src    └────┘└────────────────────┘└─┘   └────────────┘└┘  └─────────┘
typ    └────┘└────────────────────┘└─┘   └────────────┘└┘ └─────────┘
doc    └────┘                      └─┘   └────────────┘└┘   └─────────┘
txt    └────┘                      └─┘   └────────────┘└┘   └─────────┘
par    └────┘                      └─┘   └────────────┘└┘   └─────────┘
pid                               └─┘   └───────────────┘   └────────┘
st   ───────────────────────────────────┘└─────────────┘└───────────────┘└─
200    existsi n,
id             
src    └──────┘
typ    └──────┘
doc    └──────┘
txt    └──────┘
par    └──────┘
pid           
st   ──────────┘└─
201    apply div_lt_of_mul_lt_of_pos,
id           └─────────────────────┘
src    └────┘└─────────────────────┘
typ    └────┘└─────────────────────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ──────────────────────────────┘└─
202    { simp, apply add_pos_of_pos_of_nonneg zero_lt_one, apply nat.cast_nonneg },
id                   └──────────────────────┘ └─────────┘        └─────────────┘
src      └──┘  └────┘└──────────────────────┘└─────────┘  └────┘└─────────────┘
typ      └──┘  └────┘└──────────────────────┘└─────────┘  └────┘└─────────────┘
doc      └──┘  └────┘                                     └────┘               
txt      └──┘  └────┘                                     └────┘               
par      └──┘  └────┘                                     └────┘               
pid                                                                          
st   ───┘└──┘└──────────────────────────────────────────┘└──────────────────────┘└┘
203    { apply (div_lt_iff' hε).1,
id              └─────────┘ └┘
src      └────┘ └─────────┘  └─┘
typ      └────┘ └─────────┘└┘└─┘
doc      └────┘              └─┘
txt      └────┘              └─┘
par      └────┘              └─┘
pid                         └┘
st   ───────────────────────────┘└─
204      transitivity,
src      └──────────┘
typ      └──────────┘
doc      └──────────┘
txt      └──────────┘
par      └──────────┘
st   ───────────────┘└─
205      { exact hn },
id               └┘
src        └────┘  
typ        └────┘└┘
doc        └────┘  
txt        └────┘  
par        └────┘  
pid               
st   ─────┘└───────┘└┘
206      { simp [zero_lt_one] }}
id               └─────────┘
src        └────┘└─────────┘└┘
typ        └────┘└─────────┘└┘
doc        └────┘           └┘
txt        └────┘           └┘
par        └────┘           └┘
pid                       
st   ────────────────────────┘└──
207  end
st   ──┘
208  
209  theorem exists_pos_rat_lt {x : α} (x0 : 0 < x) : ∃ q : ℚ, 0 < q ∧ (q : α) < x :=
id                                                                   
src                                                                      
typ                                                                  
doc                                                         
210  by simpa only [rat.cast_pos] using exists_rat_btwn x0
id                  └──────────┘        └─────────────┘ └┘
src     └──────────┘└──────────┘└──────┘└─────────────┘  
typ     └──────────┘└──────────┘└──────┘└─────────────┘└┘
doc     └──────────┘            └──────┘                 
txt     └──────────┘            └──────┘                 
par     └──────────┘            └──────┘                 
pid          └──┘└┘            └────┘                 
st     └───────────────────────────────────────────────────
211  
src  
typ  
doc  
txt  
par  
pid  
st   
212  include α
213  @[simp] theorem rat.cast_floor (x : ℚ) :
id                                       
src                                      
typ                                      
doc    └──┘                              
214    by haveI := archimedean.floor_ring α; exact ⌊(x:α)⌋ = ⌊x⌋ :=
id                 └────────────────────┘                
src       └───────┘└────────────────────┘   └────┘      
typ       └───────┘└────────────────────┘  └────┘    
doc       └───────┘                         └────┘       
txt       └───────┘                         └────┘         
par       └───────┘                         └────┘         
pid            └─┘                                       
st       └──────────────────────────────────────────────────────┘
215  begin
st   └─────
216    haveI := archimedean.floor_ring α,
id              └────────────────────┘ 
src    └───────┘└────────────────────┘
typ    └───────┘└────────────────────┘
doc    └───────┘                      
txt    └───────┘                      
par    └───────┘                      
pid         └─┘                      
st   ──────────────────────────────────┘└─
217    apply le_antisymm,
id           └─────────┘
src    └────┘└─────────┘
typ    └────┘└─────────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ──────────────────┘└─
218    { rw [le_floor, ← @rat.cast_le α, rat.cast_coe_int],
id           └──────┘     └─────────┘   └──────────────┘
src      └──┘└──────┘└──┘ └─────────┘ └┘└──────────────┘
typ      └──┘└──────┘└──┘ └─────────┘└┘└──────────────┘
doc      └──┘        └──┘             └┘                
txt      └──┘        └──┘             └┘                
par      └──┘        └──┘             └┘                
pid        └┘        └──┘             └┘                
st   ───┘└──────────┘└────────────────┘└────────────────┘└──
219      apply floor_le },
id             └──────┘
src      └────┘└──────┘
typ      └────┘└──────┘
doc      └────┘        
txt      └────┘        
par      └────┘        
pid                   
st   ──────────────────┘└┘
220    { rw [le_floor, ← rat.cast_coe_int, rat.cast_le],
id           └──────┘    └──────────────┘  └─────────┘
src      └──┘└──────┘└──┘└──────────────┘└┘└─────────┘
typ      └──┘└──────┘└──┘└──────────────┘└┘└─────────┘
doc      └──┘        └──┘                └┘           
txt      └──┘        └──┘                └┘           
par      └──┘        └──┘                └┘           
pid        └┘        └──┘                └┘           
st   ───────────────┘└──────────────────┘└───────────┘└──
221      apply floor_le }
id             └──────┘
src      └────┘└──────┘
typ      └────┘└──────┘
doc      └────┘        
txt      └────┘        
par      └────┘        
pid                   
st   ──────────────────┘└─
222  end
st   ──┘
223  
224  end linear_ordered_field
225  
226  section
227  variables [discrete_linear_ordered_field α]
id              └───────────────────────────┘
src             └───────────────────────────┘
typ             └───────────────────────────┘
228  
229  /-- `round` rounds a number to the nearest integer. `round (1 / 2) = 1` -/
230  def round [floor_ring α] (x : α) : ℤ := ⌊x + 1 / 2⌋
id              └────────┘                      
src             └────────┘                         
typ             └────────┘                      
doc             └────────┘                            
231  
232  lemma abs_sub_round [floor_ring α] (x : α) : abs (x - round x) ≤ 1 / 2 :=
id                        └────────┘            └─┘    └───┘      
src                       └────────┘              └─┘     └───┘       
typ                       └────────┘            └─┘    └───┘      
doc                       └────────┘                       └───┘
233  begin
st   └─────
234    rw [round, abs_sub_le_iff],
id         └───┘  └────────────┘
src    └──┘└───┘└┘└────────────┘
typ    └──┘└───┘└┘└────────────┘
doc    └──┘└───┘└┘              
txt    └──┘     └┘              
par    └──┘     └┘              
pid      └┘     └┘              
st   ──────────┘└──────────────┘└──
235    have := floor_le (x + 1 / 2),
id             └──────┘      
src    └──────┘└──────┘  └─┘└─┘
typ    └──────┘└──────┘ └─┘└─┘
doc    └──────┘           └─┘ └─┘
txt    └──────┘           └─┘ └─┘
par    └──────┘           └─┘ └─┘
pid    └───┘└─┘           └─┘ └─┘
st   ─────────────────────────────┘└─
236    have := lt_floor_add_one (x + 1 / 2),
id             └──────────────┘  
src    └──────┘└──────────────┘   └─┘ └─┘
typ    └──────┘└──────────────┘  └─┘ └─┘
doc    └──────┘                   └─┘ └─┘
txt    └──────┘                   └─┘ └─┘
par    └──────┘                   └─┘ └─┘
pid    └───┘└─┘                   └─┘ └─┘
st   ─────────────────────────────────────┘└─
237    split; linarith
src    └───┘  └───────┘
typ    └───┘  └───────┘
doc    └───┘  └───────┘
txt    └───┘  └───────┘
par    └───┘  └───────┘
pid                   
st   ─────────────────┘
238  end
st   └─┘
239  
240  variable [archimedean α]
id             └─────────┘
src            └─────────┘
typ            └─────────┘
241  
242  theorem exists_rat_near (x : α) {ε : α} (ε0 : 0 < ε) :
id                                                  
src                                                  
typ                                                 
243    ∃ q : ℚ, abs (x - q) < ε :=
id           └─┘       
src          └─┘        
typ          └─┘       
doc          
244  let ⟨q, h₁, h₂⟩ := exists_rat_btwn $
id   └─┘    └┘  └┘     └─────────────┘
src                     └─────────────┘
typ  └─┘    └┘  └┘     └─────────────┘
245    lt_trans ((sub_lt_self_iff x).2 ε0) ((lt_add_iff_pos_left x).2 ε0) in
id     └──────┘   └─────────────┘    └┘    └─────────────────┘    └┘
src    └──────┘   └─────────────┘           └─────────────────┘   
typ    └──────┘   └─────────────┘    └┘    └─────────────────┘    └┘
246  ⟨q, abs_sub_lt_iff.2 ⟨sub_lt.1 h₁, sub_lt_iff_lt_add.2 h₂⟩⟩
id       └────────────┘   └────┘      └───────────────┘
src      └────────────┘   └────┘      └───────────────┘
typ      └────────────┘   └────┘      └───────────────┘
247  
248  instance : archimedean ℚ :=
id              └─────────┘ 
src             └─────────┘ 
typ             └─────────┘ 
doc                         
249  archimedean_iff_rat_le.2 $ λ q, ⟨q, by rw rat.cast_id⟩
id   └────────────────────┘                 └─────────┘
src  └────────────────────┘                └─┘└─────────┘
typ  └────────────────────┘              └─┘└─────────┘
doc                                         └─┘
txt                                         └─┘
par                                         └─┘
pid                                           
st                                         └─────────────┘
250  
251  @[simp] theorem rat.cast_round (x : ℚ) : by haveI := archimedean.floor_ring α;
id                                                       └────────────────────┘ 
src                                             └───────┘└────────────────────┘
typ                                             └───────┘└────────────────────┘
doc    └──┘                                     └───────┘                      
txt                                              └───────┘                      
par                                              └───────┘                      
pid                                                   └─┘                      
st                                              └───────────────────────────────────
252    exact round (x:α) = round x :=
id                       └───┘ 
src    └────┘        └┘└───┘ 
typ    └────┘       └┘└───┘
doc    └────┘        └┘ └───┘ 
txt    └────┘        └┘       
par    └────┘        └┘       
pid                 └┘       
st   ─────────────────────────────┘
253  have ((x + (1 : ℚ) / (2 : ℚ) : ℚ) : α) = x + 1 / 2, by simp,
id                                        
src                                                 └──┘
typ                                              └──┘
doc                                                      └──┘
txt                                                         └──┘
par                                                         └──┘
st                                                         └───┘
254  by rw [round, round, ← this, rat.cast_floor]
id          └───┘  └───┘    └──┘  └────────────┘
src     └──┘└───┘└┘└───┘└──┘    └┘└────────────┘└─
typ     └──┘└───┘└┘└───┘└──┘└──┘└┘└────────────┘└─
doc     └──┘└───┘└┘└───┘└──┘    └┘              └─
txt     └──┘     └┘     └──┘    └┘              └─
par     └──┘     └┘     └──┘    └┘              └─
pid       └┘     └┘     └──┘    └┘              
st     └────────┘└─────┘└──────┘└──────────────┘
255  
src  
typ  
doc  
txt  
par  
pid  
st   
256  end